package tableaux.rules;

import java.util.ArrayList;
import java.util.Collections;
import java.util.Comparator;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;

import tableaux.BranchChanges;
import tableaux.Branching;
import tableaux.Completion;

import entities.Individual;
import entities.concept.Concept;
import entities.concept.Nominal;
import entities.role.Role;

/**
 * Given a nominal in an individual, test if other individuals have this nominal
 * as well. If yes, merge them.
 * 
 * @author j55wu
 * 
 */
public class RuleNominal {
	private Completion dc;
	private Nominal nextExp;
	private Branching br;
	private BranchChanges brc;
	private Set<Individual> pruned;

	public RuleNominal(Completion dc) {
		super();
		this.dc = dc;
		this.br = this.dc.getCurrentBranching();
	}

	public boolean isApplicable(Individual n) {
		// only applicable to nominal nodes
		if (n.isBlockable()) {
			return false;
		}
		HashSet<Concept> unexp = new HashSet<Concept>();
		unexp.addAll(n.getLabels());
		unexp.removeAll(n.getExpandedLabels());
		if (unexp.size() < 1) {
			return false;
		}
		for (Concept c : unexp) {
			if (c instanceof Nominal) {
				Nominal nom = (Nominal) c;
				// check if nom appears in >= 2 non-different nodes
				if (nom.appearInNodes().size() >= 2) {
					this.nextExp = nom;
					return true;
				}
			}
		}
		return false;
	}

	private enum mergeOrder {
		pruneNewestNodes, pruneOldestNodes, selectCurrentNode
	}

	// new nodes usually have fewer relationships and labels to be merged
	// Old nodes usually might prune more blockable successors [Problematic in
	// practice]
	mergeOrder defMergeOrder = mergeOrder.pruneOldestNodes;

	public boolean applyRule(Individual n) {
		this.pruned = new HashSet<Individual>();
		boolean suc = false;
		// the first is the basic one, all others are merged to it.
		List<Individual> nodes = new ArrayList<Individual>();
		nodes.addAll(this.nextExp.appearInNodes());
		Individual basis = null;
		if (defMergeOrder.equals(mergeOrder.pruneNewestNodes)) {
			Collections.sort(nodes, new Comparator<Individual>() {
				public int compare(Individual n1, Individual n2) {
					return n1.getOrder() - n2.getOrder();
				}
			});
			basis = nodes.remove(0);
		} else if (defMergeOrder.equals(mergeOrder.pruneOldestNodes)) {
			Collections.sort(nodes, new Comparator<Individual>() {
				public int compare(Individual n1, Individual n2) {
					return n2.getOrder() - n1.getOrder();
				}
			});
			basis = nodes.remove(0);
		} else if (defMergeOrder.equals(mergeOrder.selectCurrentNode)) {
			// all other nodes are merged into the node being reasoned
			if (nodes.contains(n)) {
				basis = n;
				nodes.remove(n);
			} else {
				// randomly selected
				basis = nodes.remove(0);
			}
		}

		for (int i = 0; i < nodes.size(); i++) {
			Individual m = nodes.get(i);
			if (!m.isDifferentFrom(basis) && !this.pruned.contains(m)) {
				suc |= this.mergeNodes(nextExp, m, basis);
			}
		}
		boolean expadd = n.addExpandedLabels(this.nextExp);
		if (expadd && BranchChanges.getRecordingStatus()) {
			brc = br.getBranchChanges();
			brc.addToExpandedLabel(n, this.nextExp);
		}
		this.purge();
		return suc;
	}

	// remove a quadruple <a R b type>
	private void processEntries(Individual a, Role r, Individual b,
			BranchChanges.modType type) {
		boolean record = BranchChanges.getRecordingStatus();
		boolean pro = false;
		switch (type) {
		case ADD_PARENT:
			pro = a.addParents(r, b);
			break;
		case ADD_CHILD:
			pro = a.addChild(r, b);
			break;
		case RM_PARENT:
			pro = a.removeParents(r, b);
			break;
		case RM_CHILD:
			pro = a.removeChild(r, b);
			break;
		}
		if (pro && record) {
			brc = br.getBranchChanges();
			brc.updateRoleRelations(a, r, b, type);
		}
	}

	/*
	 * Merge a into b, i.e., only b is active after merging. After merging, must
	 * put b back in queue for further reasoning.
	 */
	private boolean mergeNodes(Nominal nom, Individual a, Individual b) {
		if (true) {
			System.out.println("\nTry to merge node ["
					+ (a.isSat() ? "sat" : "unsat") + "]" + a + " ---> " + b
					+ " because of " + nom);
			System.out.println("labels from a: " + a.getLabels());
			System.out.println("labels from b: " + b.getLabels());
		}
		boolean modified = false, record = BranchChanges.getRecordingStatus();
		// point all parents of a to b: pa->b
		Map<Role, HashSet<Individual>> pmap = new HashMap<Role, HashSet<Individual>>();
		pmap.putAll(a.getParentsMap());
		for (Role r : pmap.keySet()) {
			for (Individual pa : pmap.get(r)) {
				Role ir = dc.getInitTBox().getRoleBox().getInverseRole(r);
				modified |= true;
				this.processEntries(b, r, pa, BranchChanges.modType.ADD_PARENT);
				this.processEntries(pa, r, b, BranchChanges.modType.ADD_CHILD);
				this.processEntries(b, ir, pa, BranchChanges.modType.ADD_CHILD);
				this.processEntries(pa, ir, b, BranchChanges.modType.ADD_PARENT);
				// remove all incoming edges to a, outgoing edge to be handled
				// later
				this.processEntries(a, r, pa, BranchChanges.modType.RM_PARENT);
				this.processEntries(pa, r, a, BranchChanges.modType.RM_CHILD);
			}

		}
		// point all *nominal* children of a to b: b->ca
		Map<Role, HashSet<Individual>> cmap = new HashMap<Role, HashSet<Individual>>();
		cmap.putAll(a.getChildrenMap());
		for (Role r : cmap.keySet()) {
			for (Individual ca : cmap.get(r)) {
				if (!ca.isNominalNode()) {
					continue;
				}
				Role ir = dc.getInitTBox().getRoleBox().getInverseRole(r);
				modified |= true;
				this.processEntries(ca, r, b, BranchChanges.modType.ADD_PARENT);
				this.processEntries(b, r, ca, BranchChanges.modType.ADD_CHILD);
				this.processEntries(ca, ir, b, BranchChanges.modType.ADD_CHILD);
				this.processEntries(b, ir, ca, BranchChanges.modType.ADD_PARENT);
				// remove nominal connections
				this.processEntries(ca, r, a, BranchChanges.modType.RM_PARENT);
				this.processEntries(a, r, ca, BranchChanges.modType.RM_CHILD);
			}
		}
		// TODO:copy all the labels of a, may need a CLEAN copy, i.e., not
		// expanded/original
		for (Concept al : a.getLabels()) {
			if (b.addLabels(al)) {
				modified |= true;
				if (record) {
					brc = br.getBranchChanges();
					brc.addToLabel(b, al);
				}
			}
		}
		// if(record){
		// brc = br.getBranchChanges();
		// brc.addToLabel(b, a.getLabels());
		// }
		// TODO:keep unequal pairs
		nom.removeAttachedIndividual(a);
		if (record) {
			brc = br.getBranchChanges();
			brc.rmNominalInds(nom, a);
		}
		modified |= this.prune(a);
		return modified;
	}

	private boolean prune(Individual m) {
		boolean ret = false, record = BranchChanges.getRecordingStatus();
		// prune all outgoing edges of m->n
		for (Individual n : m.getChildren()) {
			Set<Role> rs = m.relatedRoleForChild(n);
			for (Role r : rs) {
				this.processEntries(n, r, m, BranchChanges.modType.RM_PARENT);
				this.processEntries(m, r, n, BranchChanges.modType.RM_CHILD);
			}
			if (n.isBlockable()) {
				ret |= prune(n);
			}
		}
		// remove m from the completion graph
		if (this.dc.removeIndividualFromQueue(m) && record) {
			brc.updateQueueInds(m, -1);
			ret |= true;
		}
		System.err.println("Pruned: " + m);
		this.pruned.add(m);
		return ret;
	}

	// if a node is pruned, this node should not be referenced anywhere.
	private void purge() {
		// remove m from attached nominals
		for (Individual m : this.pruned) {
			for (Nominal n : m.getNominals()) {
				// System.err.println("Purged from nominal "+n+" of nodes:"+m);
				if (n.removeAttachedIndividual(m)
						&& BranchChanges.getRecordingStatus()) {
					br.getBranchChanges().rmNominalInds(n, m);
				}
			}
		}
		pruned.clear();
	}

}
